$\forall$${\it es}$:ES, $p$:(E$\rightarrow$(E + Top)). causal{-}predecessor(${\it es}$;$p$) $\Rightarrow$ SWellFounded(p{-}graph(E;$p$)($y$,$x$))